[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
data asm specification
ebm
using ebm-base
procedures ebm_get_volume_size# volid × abstract-volumes : : nat ;
ebm_create_volume# volid × nat : abstract-volumes : error nondeterministic;
ebm_read# volid × nat × nat × nat × nat × abstract-volumes : buffer : error nondeterministic;
ebm_write# volid × nat × nat × nat × nat × buffer : abstract-volumes : error nondeterministic;
ebm_erase# volid × nat : abstract-volumes : error nondeterministic;
ebm_unmap# volid × nat : abstract-volumes nonfunctional ;
ebm_map# volid × nat : abstract-volumes : error nondeterministic;
ebm_change# volid × nat × nat × buffer : abstract-volumes : error nondeterministic;
ebm_sync_device# abstract-volumes : : error nondeterministic;
ebm_get_page_size# abstract-volumes : : nat ;
ebm_get_leb_size# abstract-volumes : : nat ;
ebm_format# : : abstract-volumes × error nondeterministic;
ebm_recover# : abstract-volumes : error nondeterministic;
variables ERR : error flexible;
ERR0 : error flexible;
AVOLS : abstract-volumes flexible;
AVOLS0 : abstract-volumes flexible;
BUF : buffer flexible;
BUF0 : buffer flexible;
VOLID : volid flexible;
VOLID0 : volid flexible;
LNUM : nat flexible;
OFFSET : nat flexible;
N : nat flexible;
N0 : nat flexible;
N1 : nat flexible;
state variables AVOLS : abstract-volumes flexible;
initialization procedure ebm_format#
if ERR = ESUCCESS
sequential
invariants inv : ⊦ ebm-cons(AVOLS);
crash predicate AVOLS` ⊆ AVOLS ∧ (ebm-cons(AVOLS`) → ebm-cons(AVOLS))
with crash-neutrality
recovery procedure ebm_recover#
if ERR = ESUCCESS
declarations get-volume-size:
ebm_get_volume_size#(VOLID, AVOLS; ; N)
precondition VOLID ∈ AVOLS;
postcondition true;
{if VOLID ∈ AVOLS then N := # AVOLS[VOLID] else abort
}
create-volume:
ebm_create_volume#(VOLID, N; AVOLS; ERR)
precondition ¬ VOLID ∈ AVOLS;
postcondition true;
{if ¬ VOLID ∈ AVOLS
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOLS[VOLID] := fill(mkabstractvolume(N), erased)}
else abort
}
read:
ebm_read#(VOLID, LNUM, OFFSET, N0, N, AVOLS; BUF; ERR)
precondition VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF;
postcondition true;
{if VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then if ¬ AVOLS[VOLID][LNUM].mapped?
then BUF := fill(BUF, empty, N0, N)
else BUF := copy(AVOLS[VOLID][LNUM].data, OFFSET, BUF, N0, N)
else choose BUF0
with # BUF0 = # BUF ∧ range=(BUF0, 0, BUF, 0, N0) ∧ range=(BUF0, N0 + N, BUF, N0 + N, # BUF - N0 + N)
in BUF := BUF0}
else abort
}
write:
ebm_write#(VOLID, LNUM, OFFSET, N0, N, BUF; AVOLS; ERR)
precondition VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ is-aligned(OFFSET, EB_PAGE_SIZE)
∧ is-aligned(N, EB_PAGE_SIZE) ∧ N + N0 ≤ # BUF ∧ (AVOLS[VOLID][LNUM].mapped? → OFFSET ≥ AVOLS[VOLID][LNUM].fill)
;
postcondition true;
{if VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ is-aligned(OFFSET, EB_PAGE_SIZE)
∧ is-aligned(N, EB_PAGE_SIZE) ∧ N + N0 ≤ # BUF ∧ (AVOLS[VOLID][LNUM].mapped? → OFFSET ≥ AVOLS[VOLID][LNUM].fill)
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then if AVOLS[VOLID][LNUM].mapped?
then if N ≠ 0
then AVOLS[VOLID][LNUM]
:= mapped
(subarray(AVOLS[VOLID][LNUM].data, 0, OFFSET) + subarray(BUF, N0, N) + mkempbuf(LEB_SIZE - OFFSET - N),
OFFSET + N)
else AVOLS[VOLID][LNUM] := mapped(mkempbuf(OFFSET) + subarray(BUF, N0, N) + mkempbuf(LEB_SIZE - OFFSET - N), OFFSET + N)
else if AVOLS[VOLID][LNUM].mapped?
then choose N1
with N1 < N ∧ is-aligned(N1, EB_PAGE_SIZE)
in if N1 ≠ 0
then AVOLS[VOLID][LNUM]
:= mapped
(subarray(AVOLS[VOLID][LNUM].data, 0, OFFSET) + subarray(BUF, N0, N1) + mkempbuf(LEB_SIZE - OFFSET - N1),
OFFSET + N1)
ifnone skip
else if N ≠ 0 then AVOLS[VOLID][LNUM] := unmapped}
else abort
}
erase:
ebm_erase#(VOLID, LNUM; AVOLS; ERR)
precondition VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID];
postcondition true;
{if VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID]
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS then AVOLS[VOLID][LNUM] := erased else {skip or AVOLS[VOLID][LNUM] := unmapped}}
else abort
}
unmap:
ebm_unmap#(VOLID, LNUM; AVOLS)
precondition VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID];
postcondition true;
{if VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] then AVOLS[VOLID][LNUM] := unmapped else abort
}
map:
ebm_map#(VOLID, LNUM; AVOLS; ERR)
precondition VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] ∧ ¬ AVOLS[VOLID][LNUM].mapped?;
postcondition true;
{if VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] ∧ ¬ AVOLS[VOLID][LNUM].mapped?
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOLS[VOLID][LNUM] := mapped(emptyleb, 0)}
else abort
}
change:
ebm_change#(VOLID, LNUM, N, BUF; AVOLS; ERR)
precondition VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] ∧ N ≤ LEB_SIZE ∧ N ≤ # BUF ∧ is-aligned(N, EB_PAGE_SIZE);
postcondition true;
{if VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] ∧ N ≤ LEB_SIZE ∧ N ≤ # BUF ∧ is-aligned(N, EB_PAGE_SIZE)
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS then AVOLS[VOLID][LNUM] := mapped(subarray(BUF, 0, N) + mkempbuf(LEB_SIZE - N), N)}
else abort
}
sync-device:ebm_sync_device#(AVOLS; ; ERR) precondition true; postcondition true;{fail_or_success#(; ; ERR)}
get-page-size:ebm_get_page_size#(AVOLS; ; N) precondition true; postcondition true;{N := EB_PAGE_SIZE}
get-leb-size:ebm_get_leb_size#(AVOLS; ; N) precondition true; postcondition true;{N := LEB_SIZE}
format:
ebm_format#(; ; AVOLS, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOLS := ∅ else AVOLS := ?}
}
recover:
ebm_recover#(; AVOLS; ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR ≠ ESUCCESS then AVOLS := ?}
}
end data asm specification